/**
 * <vendor>
 *  Copyright 2009 Quanben Tech.
 * </vendor>
 */

using System;
using System.Text;
using System.Collections;
using System.Collections.Generic;
using QSharp.String.Compiler;


namespace QSharp.String.Rex
{
    /**
     * <summary>
     *  Regular Machine
     * </summary>
     */
    public class Machine<Stream> : IDisposable
        where Stream : ITokenStream 
    {
    /* constants */
        public const uint MaxUint = 0xffffffff;

    /* exceptions */
        class UnknownStateException : ApplicationException
        {
            public UnknownStateException()
                : base("UnknownStateException")
            {
            }
        }

    /* embedded types */
        public interface IState : IEnumerable<IArrow>
        {
            uint Id { get; }

            uint OutletCount { get; }

            void AddOutlet(IArrow arrow);

            IArrow GetOutlet(int i);
        }

        public abstract class State : IState, IDisposable
        {
            public virtual uint Id
            {
                get
                {   // by default we use hashcode as id which of two different states may unify
                    return (uint)this.GetHashCode();
                }
            }

            protected bool mDisposed = false;

            public abstract uint OutletCount { get; }

            IEnumerator IEnumerable.GetEnumerator()
            {
                return GetEnumerator();
            }

            public abstract IEnumerator<IArrow> GetEnumerator();

            public override string ToString()
            {
                return string.Format("State[0x{0:X8}]", Id);
            }

            public abstract void AddOutlet(IArrow arrow);
            public abstract IArrow GetOutlet(int i);

            protected virtual void Dispose(bool disposing)
            {
                if (!mDisposed)
                {
                    /* below is more like a template with instructions as remarks */
                    if (disposing)
                    {   // Ok to reference objects
                    }
                    // clean up here
                    mDisposed = true;
                }
            }

            public void Dispose()
            {
                Dispose(true);
                GC.SuppressFinalize(this);
            }

            ~State()
            {
                Dispose(false);
            }
        }   /* class State */

        public interface IArrow    /* transition between state */
        {
            IState Go(Stream stream);
            IState Target { get; }
        }

        public abstract class Arrow : IArrow, IDisposable
        {
            protected bool mDisposed = false;

            public abstract IState Go(Stream stream);
            public abstract IState Target { get; set; }

            protected virtual void Dispose(bool disposing)
            {
                if (!mDisposed)
                {
                    /* below is more like a template with instructions as remarks */
                    if (disposing)
                    {   
                        // clean up managed objects
                        IDisposable target = Target as IDisposable;
                        if (target != null)
                        {
                            target.Dispose();
                        }
                    }
                    // clean up unmanaged objects
                    // ...
                    mDisposed = true;
                }
            }

            public void Dispose()
            {
                Dispose(true);
                GC.SuppressFinalize(this);
            }

            ~Arrow()
            {
                Dispose(false);
            }
        }

        /**
         * <summary>
         *  The set of iteration count allowed
         * </summary>
         */
        public class Iteration : SegmentedSet<WrappedUint>
        {
            public static uint Infinity
            {
                get
                {
                    return MaxUint;
                }
            }

            public uint MaxTimes
            {
                get
                {
                    int n = mData.Count;
                    if (n == 0) return Infinity;
                    return mData[n-1].High;
                }
            }

            public uint MinTimes
            {
                get
                {
                    int n = mData.Count;
                    if (n == 0) return 0;
                    return mData[0].Low;
                }
            }

            public bool AllowLeave(uint niter)
            {
                return Contains((WrappedUint)niter);
            }
        }

        public class TerminalState : State
        {
            public override uint OutletCount { get { return 0; } }

            public override IEnumerator<IArrow> GetEnumerator() // State
            {
                for ( int i = 0; i != 0; )
                    yield return null;
            }

            public override void AddOutlet(IArrow arrow)
            {
                throw new InvalidOperationException();
            }

            public override IArrow GetOutlet(int i)
            {
                return null;
            }

            public override string ToString()
            {
                StringBuilder sb = new StringBuilder(base.ToString());
                sb.Append(" : Terminal");
                return sb.ToString();
            }
        }

        public class FanoutState : State
        {
            public List<IArrow> Outlets = new List<IArrow>();

            public override uint OutletCount { get { return (uint)Outlets.Count; } }

            public IState Go(Stream stream, int iout)
            {
                return Outlets[iout].Go(stream);
            }

            public override IEnumerator<IArrow> GetEnumerator() // State
            {
                return Outlets.GetEnumerator();
            }

            public override void AddOutlet(IArrow arrow)
            {
                Outlets.Add(arrow);
            }

            public override IArrow GetOutlet(int i)
            {
                return Outlets[i];
            }

            public override string ToString()
            {
                StringBuilder sb = new StringBuilder(base.ToString());
                sb.Append(" : Fanout");
                return sb.ToString();
            }
        }

        public class RelayState : State
        {
            public IArrow Outlet = null;
            public override uint OutletCount { get { return (uint)((Outlet == null) ? 0 : 1); } }

            public IState Go(Stream stream, int iout)
            {
                return Outlet.Go(stream);
            }

            public override IEnumerator<IArrow> GetEnumerator() // State
            {
                yield return Outlet;
            }

            public override void AddOutlet(IArrow arrow)
            {
                Outlet = arrow;
            }

            public override IArrow GetOutlet(int i)
            {
                if (i > 0) throw new IndexOutOfRangeException();
                return Outlet;
            }

            public override string ToString()
            {
                StringBuilder sb = new StringBuilder(base.ToString());
                sb.Append(" : Relay");
                return sb.ToString();
            }
        }

        /**
         * <summary>
         *  The trap in which iteration is made
         * </summary>
         */
        public class TrapState : State
        {
            public IArrow Loop = null;
            public IArrow Leave = null;
            public Iteration Iteration = null;  // null for any times

            public uint MaxTimes
            {
                get
                {
                    if (Iteration == null)
                        return Iteration.Infinity;
                    else
                        return Iteration.MaxTimes;
                }
            }

            public uint MinTimes
            {
                get
                {
                    if (Iteration == null)
                        return 0;
                    else
                        return Iteration.MinTimes;
                }
            }

            public override uint OutletCount 
            { 
                get 
                {
                    if (Loop == null) return 0;
                    if (Leave == null) return 1;
                    return 2;
                } 
            }

            public bool AllowLeave(uint niter)
            {
                if (Iteration == null)
                    return true;
                return Iteration.AllowLeave(niter);
            }

            public IState Go(Stream stream, bool loop)
            {
                if (loop) return Loop.Go(stream);
                else return Leave.Go(stream);
            }

            public override IEnumerator<IArrow> GetEnumerator() // State
            {
                yield return Loop;
                yield return Leave;
            }

            public override void AddOutlet(IArrow arrow)
            {
                if (Loop == null) Loop = arrow;
                else Leave = arrow;
            }

            public override IArrow GetOutlet(int i)
            {
                if (i == 0) return Loop;
                if (i == 1) return Leave;
                throw new IndexOutOfRangeException();
            }

            public override string ToString()
            {
                StringBuilder sb = new StringBuilder(base.ToString());
                sb.Append(" : Trap");
                return sb.ToString();
            }
        }   /* class TrapState */

        /**
         * <remarks>
         *  It is used for back-referencing
         * </remarks>
         */
        public abstract class TaggedState : FanoutState
        {
            public TagTracker Tag = null;

            public abstract void Bind(TokenStream.Position p);
        }

        public class TagOpenState : TaggedState
        {
            public override void Bind(TokenStream.Position p)
            {
                if (Tag != null)
                {
                    Tag.BindStart((TokenStream.Position)p.Clone());
                }
            }

            public override string ToString()
            {
                StringBuilder sb = new StringBuilder(base.ToString());
                sb.Append(".TagOpen");
                return sb.ToString();
            }
        }

        public class TagCloseState : TaggedState
        {
            public override void Bind(TokenStream.Position p)
            {
                if (Tag != null)
                    Tag.BindEnd((TokenStream.Position)p.Clone());
            }

            public override string ToString()
            {
                StringBuilder sb = new StringBuilder(base.ToString());
                sb.Append(".TagClose");
                return sb.ToString();
            }
        }

        struct Context
        {
            public IState State;
            public TrapRepStack TRStack;
            public int IOut;
            public Stream Stream;
        }


        /**
         * <remarks>
         * </remarks>
         */
        class TrapRep : ICloneable
        {
            public TrapState State = null;
            public TokenStream.Position Pos = null;
            public uint Rep = 0;
            public int TSDepth = 0;

            public TrapRep(TrapState state, Stream stream, uint rep, int tsdepth)
            {
                State = state;
                Rep = rep;
                TSDepth = tsdepth;
                Pos = (TokenStream.Position)stream.Pos.Clone();
            }

            public TrapRep(TrapState state, TokenStream.Position pos, uint rep, int tsdepth)
            {
                State = state;
                Rep = rep;
                TSDepth = tsdepth;
                Pos = pos;
            }

            protected TrapRep()
            {
            }

            public void UpdateStream(Stream stream)
            {
                Pos = (TokenStream.Position)stream.Pos.Clone();
            }

            public object Clone()
            {
                TrapRep res = new TrapRep();
                res.State = this.State;
                res.Pos = this.Pos;
                res.Rep = this.Rep;
                return res;
            }
        }

        class TrapRepStack : Stack<TrapRep>, ICloneable
        {
            public TrapRep GetTop()
            {
                if (Count == 0)
                    return null;
                return Peek();
            }

            public Object Clone()
            {
                TrapRepStack res = new TrapRepStack();
                TrapRep[] temp = this.ToArray();
                for (int i = temp.Length - 1; i >= 0; i--)
                {
                    res.Push(temp[i].Clone() as TrapRep);
                }
                return res;
            }
        }

        /**
         * <remarks>
         * </remarks>
         */
        class TrapRepUndoStack : Stack<TrapRepUndoStack.TrapRepUndo>
        {
            public class TrapRepUndo
            {
                public TrapState State;

                public TrapRepUndo(TrapState state)
                {
                    State = state;
                }
            }

            protected class TrapRepPopUndo : TrapRepUndo
            {
                public TrapRepPopUndo(TrapState state)
                    : base(state)
                {
                }
            }

            protected class TrapRepSetUndo : TrapRepUndo
            {
                public enum Type
                {
                    Mod,
                    Push,
                }

                public Type Op;
                public TokenStream.Position Pos;
                public uint Rep;
                public int TSDepth;

                public TrapRepSetUndo(Type op, TrapState state, TokenStream.Position pos, uint rep, int tsdepth) 
                    : base(state)
                {
                    Op = op;
                    Pos = pos;  // no need to clone
                    Rep = rep;
                    TSDepth = tsdepth;
                }

                public void SetTrapRep(ref TrapRep tr)
                {
                    tr.State = this.State;
                    tr.Pos = this.Pos;
                    tr.Rep = this.Rep;
                    tr.TSDepth = this.TSDepth;
                }
            }

            /**
             * <remarks>
             *  Do this when the pop is made, with the TR popped out passed as poppedTR
             * </remarks>
             */
            public void MarkPop(TrapRep poppedTR)
            {
                TrapState state = poppedTR.State;
                TokenStream.Position pos = poppedTR.Pos;
                uint rep = poppedTR.Rep;
                int tsdepth = poppedTR.TSDepth;

                if (base.Count > 0 && state == base.Peek().State)
                {
                    TrapRepSetUndo trs = base.Peek() as TrapRepSetUndo;

                    if (trs != null && trs.Op == TrapRepSetUndo.Type.Mod)
                    {
                        trs.Op = TrapRepSetUndo.Type.Push;
                    }
                    else
                    {
                        System.Diagnostics.Debug.Assert(base.Peek() is TrapRepPopUndo);
                        base.Pop();
                    }
                }
                else
                {
                    base.Push(new TrapRepSetUndo(TrapRepSetUndo.Type.Push, state, pos, rep, tsdepth));
                }
            }

            /**
             * <remarks>
             *  Do this before or after the push is made 
             * </remarks>
             */
            public void MarkPush(TrapState state)
            {
                if (base.Count > 0 && state == base.Peek().State)
                {
                    TrapRepSetUndo trs = base.Peek() as TrapRepSetUndo;

                    // it can neigther be AddToHeap or Mod
                    System.Diagnostics.Debug.Assert(trs != null && trs.Op == TrapRepSetUndo.Type.Push);

                    trs.Op = TrapRepSetUndo.Type.Mod;
                }
                else
                {
                    base.Push(new TrapRepPopUndo(state));
                }
            }


            /**
             * <remarks>
             *  Do this before the modification is made, with the old TR passed as oldTR
             * </remarks>
             */
            public void MarkMod(TrapRep oldTR)
            {
                TrapState state = oldTR.State;
                TokenStream.Position pos = oldTR.Pos;
                uint rep = oldTR.Rep;
                int tsdepth = oldTR.TSDepth;

                if (base.Count > 0 && state == base.Peek().State)
                {
                    TrapRepUndo tru = base.Peek();
                    System.Diagnostics.Debug.Assert(tru is TrapRepPopUndo
                        || tru is TrapRepSetUndo && (tru as TrapRepSetUndo).Op == TrapRepSetUndo.Type.Mod);
                    // do nothing
                }
                else
                {
                    base.Push(new TrapRepSetUndo(TrapRepSetUndo.Type.Mod, state, pos, rep, tsdepth));
                }
            }

            public void Restore(ref TrapRepStack trstack)
            {
                while (this.Count > 0)
                {
                    TrapRepUndo tru = base.Pop();

                    if (tru is TrapRepPopUndo)
                    {
                        trstack.Pop();
                    }
                    else
                    {
                        TrapRepSetUndo trs = tru as TrapRepSetUndo;
                        if (trs.Op == TrapRepSetUndo.Type.Push)
                        {
                            trstack.Push(new TrapRep(trs.State, trs.Pos, trs.Rep, trs.TSDepth));
                        }
                        else if (trs.Op == TrapRepSetUndo.Type.Mod)
                        {
                            TrapRep tr = trstack.Peek();
                            trs.SetTrapRep(ref tr);
                        }
                    }
                }
            }

            protected void Merge(TrapRepUndo[] undos)
            {
                int i;
                for (i = undos.Length - 1; i >= 0; i--)
                {
                    TrapRepUndo tru = undos[i];
                    if (base.Count == 0) break;
                    TrapRepUndo top = base.Peek();

                    if (top.State == tru.State)
                    {
                        if (tru is TrapRepSetUndo)
                        {
                            TrapRepSetUndo trsu1 = tru as TrapRepSetUndo;
                            if (top is TrapRepSetUndo)
                            {
                                TrapRepSetUndo trsu2 = top as TrapRepSetUndo;
                                
                                if (trsu1.Op == TrapRepSetUndo.Type.Mod)
                                {
                                    if (trsu2.Op == TrapRepSetUndo.Type.Mod)
                                    {   // case 1: both mod
                                        // do nothing
                                    }
                                    else if (trsu2.Op == TrapRepSetUndo.Type.Push)
                                    {   // case 2: mod and push
                                        trsu1.Op = TrapRepSetUndo.Type.Push;
                                    }
                                    else
                                    {
                                        throw new UnknownStateException();
                                    }
                                }
                                else
                                {
                                    throw new UnknownStateException();
                                }
                            }
                            else
                            {   // case 3: push and pop
                                trsu1.Op = TrapRepSetUndo.Type.Mod;
                            }
                        }
                        else
                        {
                            TrapRepSetUndo trsu2 = top as TrapRepSetUndo;
                            if (trsu2 != null)
                            {
                                if (trsu2.Op == TrapRepSetUndo.Type.Mod)
                                {   // case 4: pop and mod
                                    // do nothing
                                }
                                else if (trsu2.Op == TrapRepSetUndo.Type.Push)
                                {   // case 5: pop and push
                                    base.Pop();
                                }
                                else
                                {
                                    throw new UnknownStateException();
                                }
                            }
                            else
                            {
                                throw new UnknownStateException();
                            }
                        }
                    }
                    else
                    {
                        break;
                    }
                }

                for (; i >= 0; i--)
                {
                    base.Push(undos[i]);
                }
            }

            /**
             * <remarks>
             *  It returns the TrapRepUndoStack that can recover the context to the state swapped in
             * </remarks>
             */
            public void Swap(ref TrapRepStack trstack, out TrapRepUndoStack trustack1, ref TrapRepUndoStack trustack2)
            {
                if (trustack2 != null)
                {
                    TrapRepUndo[] temp = base.ToArray();
                    trustack2.Merge(temp);
                }

                Swap(ref trstack, out trustack1);
            }

            public void Swap(ref TrapRepStack trstack, out TrapRepUndoStack trustack1)
            {
                trustack1 = new TrapRepUndoStack();
                while (this.Count > 0)
                {
                    TrapRepUndo tru = base.Pop();
                    TrapRep tr;

                    if (tru is TrapRepPopUndo)
                    {
                        tr = trstack.Pop();
                        trustack1.MarkPop(tr);
                    }
                    else
                    {
                        TrapRepSetUndo trs = tru as TrapRepSetUndo;
                        if (trs.Op == TrapRepSetUndo.Type.Push)
                        {
                            tr = new TrapRep(trs.State, trs.Pos, trs.Rep, trs.TSDepth);
                            trstack.Push(tr);
                            trustack1.MarkPush(trs.State);
                        }
                        else if (trs.Op == TrapRepSetUndo.Type.Mod)
                        {
                            tr = trstack.Peek();
                            trustack1.MarkMod(tr);
                            trs.SetTrapRep(ref tr);
                        }
                    }
                }
            }
        }   /* TrapRepUndoStack */

        class TagChangeMap : Dictionary<TagTracker, TagTracker>
        {
            /**
             * <remarks>
             *  Do this before change is made, save the target and its clone in the map
             * </remarks>
             */
            public void MarkChange(TagTracker target)
            {
                if (base.ContainsKey(target))
                {
                    return;
                }
                base[target] = (TagTracker)target.Clone();
            }

            public void Restore()
            {
                foreach (TagTracker target in base.Keys)
                {
                    TagTracker orig = base[target];
                    target.Set(orig);
                }
            }

            public void Swap(out TagChangeMap tcmap1, ref TagChangeMap tcmap2)
            {
                tcmap1 = new TagChangeMap();

                foreach (TagTracker target in base.Keys)
                {
                    TagTracker orig = base[target];
                    tcmap1.MarkChange(target);
                    target.Set(orig);

                    if (!tcmap2.ContainsKey(target))
                    {
                        tcmap2[target] = orig;
                    }
                }
            }

            public void Swap(out TagChangeMap tcmap1)
            {
                tcmap1 = new TagChangeMap();

                foreach (TagTracker target in base.Keys)
                {
                    TagTracker orig = base[target];
                    tcmap1.MarkChange(target);
                    target.Set(orig);
                }
            }
        }   /* class TagChangeMap */

        abstract class Try
        {
            public TokenStream.Position Pos;
            public TrapRepUndoStack TRUStack = new TrapRepUndoStack();
            public TagChangeMap TCMap = new TagChangeMap();

            public abstract IState Curr
            {
                get;
            }

            public Try(Stream stream)
            {
                Pos = (TokenStream.Position)stream.Pos.Clone();
            }
        }

        class FanoutTry : Try
        {
            public FanoutState State;
            public int IOut;

            public override IState Curr
            {
                get
                {
                    return State;
                }
            }

            public FanoutTry(FanoutState state, Stream stream, int iout)
                : base(stream)
            {
                State = state;
                IOut = iout;
            }
        }

        class TrapTry : Try
        {
            public TrapState State;

            public override IState Curr
            {
                get
                {
                    return State;
                }
            }

            public TrapTry(TrapState state, Stream stream) 
                : base(stream)
            {
                State = state;
            }
        }

        class TryStack : Stack<Try>
        {
            public Try GetTop()
            {
                if (base.Count == 0) return null;
                return base.Peek();
            }

            public Try PopTry()
            {
                if (base.Count == 0) return null;
                return base.Pop();
            }

            public void MarkTagChange(TagTracker target)
            {
                Try t = GetTop();
                if (t == null) return;

                t.TCMap.MarkChange(target);
            }

            public void MarkTRStackPush(TrapState state)
            {
                Try t = GetTop();
                if (t == null) return;

                t.TRUStack.MarkPush(state);
            }

            public void MarkTRStackPop(TrapRep poppedTR)
            {
                Try t = GetTop();
                if (t == null) return;

                t.TRUStack.MarkPop(poppedTR);
            }

            public void MarkTRStackMod(TrapRep oldTR)
            {
                Try t = GetTop();
                if (t == null) return;

                t.TRUStack.MarkMod(oldTR);
            }

            protected void GetContext(Try t, ref Context context)
            {
                context.State = t.Curr;
                context.Stream.Pos = t.Pos;
                t.TRUStack.Restore(ref context.TRStack);
                t.TCMap.Restore();

                if (t is FanoutTry)
                {
                    FanoutTry ft = t as FanoutTry;
                    context.IOut = ft.IOut;
                }
                else if (t is TrapTry)
                {

                    TrapTry tt = t as TrapTry;
                    TrapState curr = tt.State;

                    // leave
                    System.Diagnostics.Debug.Assert(context.TRStack.Count > 0 
                        && context.TRStack.Peek().State == curr);

                    TrapRep poppedTR = context.TRStack.Pop();
                    this.MarkTRStackPop(poppedTR);

                    context.State = curr.Go(context.Stream, false);
                }
                else
                {
                    throw new UnknownStateException();
                }
            }

            public bool PopAndRestore(ref Context context)
            {
                Try t = PopTry();
                if (t == null) return false;
                GetContext(t, ref context);
                return true;
            }

            public void Swap(ref Context context)
            {
                TrapState trap = context.State as TrapState;
                Try t = this.PopTry();

                /* set newtt */
                TrapTry newtt = new TrapTry(trap, context.Stream);
                Try t2 = this.GetTop();
                if (t2 != null)
                {
                    t.TRUStack.Swap(ref context.TRStack, out newtt.TRUStack, ref t2.TRUStack);
                    t.TCMap.Swap(out newtt.TCMap, ref t2.TCMap);
                }
                else
                {
                    t.TRUStack.Swap(ref context.TRStack, out newtt.TRUStack);
                    t.TCMap.Swap(out newtt.TCMap);
                }
                base.Push(newtt);

                /* get context */
                GetContext(t, ref context);
            }
        }   /* class TryStack */

    /* member variables */

        protected IState mStart = null;
        protected IState mEnd = null;
        protected bool mDisposed = false;

    /* properties */

        public IState Start
        {
            get
            {
                return mStart;
            }
        }

        public IState End
        {
            get
            {
                return mEnd;
            }
        }

    /* constructor/destructor */
        public Machine(IState start, IState end)
        {
            mStart = start;
            mEnd = end;
        }

        protected void Dispose(bool disposing)
        {
            if (!mDisposed)
            {
                if (disposing)
                {
                    // clean up managed objects
                    State start = mStart as State;
                    if (start != null)
                        start.Dispose();
                }
                // clean up unmanaged objects
                // ...

                mDisposed = true;
            }
        }

        public void Dispose()
        {
            Dispose(true);
            GC.SuppressFinalize(this);
        }

        ~Machine()
        {
            Dispose(false);
        }

    /* methods */

        public bool Verify(Stream stream)
        {
            TryStack stack = new TryStack();

            Context context = new Context();
            context.TRStack = new TrapRepStack();
            context.Stream = stream;
            context.State = Start;

            while (true)
            {
                Type type = context.State.GetType();

                if (context.State is RelayState)
                {
                    RelayState relay = (RelayState)context.State;
                    context.State = relay.Go(stream, 0);
                    context.IOut = 0;
                }
                else if (context.State is FanoutState)
                {
                    if (context.State is TaggedState)
                    {
                        TaggedState tagged = (TaggedState)context.State;
                        if (tagged.Tag != null)
                        {
                            stack.MarkTagChange(tagged.Tag);
                            tagged.Bind(stream.Pos);
                        }
                    }

                    FanoutState fanout = (FanoutState)context.State;
                    if (context.IOut + 1 < fanout.OutletCount)
                    {
                        stack.Push(new FanoutTry(fanout, stream, context.IOut + 1));
                    }
                    context.State = fanout.Go(stream, context.IOut);
                    context.IOut = 0;
                }
                else if (type == typeof(TrapState))
                {
                    TrapState curr = (TrapState)context.State;
                    TrapRep trtop = context.TRStack.GetTop();

                    if (trtop != null && trtop.State == curr)
                    {
                        if (trtop.Rep < curr.MaxTimes)
                        {
                            bool bAllowLeave = curr.AllowLeave(trtop.Rep);
                            bool bFinalOut = false;

                            if (bAllowLeave)
                            {
                                /* if it is an empty turn */
                                bFinalOut = trtop.Pos.Equals(stream.Pos);
                            }

                            if (bFinalOut)
                            {   /* checking if leaving with the empty turn, in favor of non-empty parsing */

                                if (stack.Count == 0)
                                {   // leave immediately
                                    TrapRep poppedTR = context.TRStack.Pop();
                                    stack.MarkTRStackPop(poppedTR);

                                    System.Diagnostics.Debug.Assert(poppedTR.State == curr);

                                    context.State = curr.Go(stream, false);
                                }
                                else
                                {
                                    if (trtop.TSDepth < stack.Count)
                                    {   // keep trying
                                        stack.Swap(ref context);
                                    }
                                    else if (trtop.TSDepth == stack.Count)
                                    {   // no chance in this coil, leave now

                                        TrapRep poppedTR = context.TRStack.Pop();
                                        stack.MarkTRStackPop(poppedTR);

                                        System.Diagnostics.Debug.Assert(poppedTR.State == curr);

                                        context.State = curr.Go(context.Stream, false);
                                    }
                                    else
                                    {
                                        throw new UnknownStateException();
                                    }
                                }
                            }
                            else 
                            {
                                stack.MarkTRStackMod(trtop);

                                trtop.Rep++;
                                trtop.UpdateStream(stream);

                                if (bAllowLeave)
                                {
                                    stack.Push(new TrapTry(curr, stream));
                                }

                                context.State = curr.Go(context.Stream, true);
                            }
                        }
                        else
                        {   // must leave
                            TrapRep poppedTR = context.TRStack.Pop();
                            stack.MarkTRStackPop(poppedTR);

                            System.Diagnostics.Debug.Assert(poppedTR.State == curr);

                            context.State = curr.Go(context.Stream, false);
                        }
                    }
                    else
                    {   /* reach the trap for the first time */

                        int tsdepth = stack.Count;
                        trtop = new TrapRep(curr, stream, 1, tsdepth);
                        context.TRStack.Push(trtop);

                        stack.MarkTRStackPush(curr);

                        if (curr.AllowLeave(0))
                        {
                            stack.Push(new TrapTry(curr, stream));
                        }

                        context.State = curr.Go(stream, true);
                    }
                }
                else if (type == typeof(TerminalState))
                {
                    return true;
                }
                else
                {
                    throw new UnknownStateException();
                }

                while (context.State == null)
                {   // recent matching failed

                    bool r = stack.PopAndRestore(ref context);
                    if (!r)
                    {
                        return false;
                    }
                }
            }
        }   /* public bool Verify(StreamType stream) */

        /**
         * <remarks>
         *  From Object. Display the machine for debug.
         * </remarks>
         */
        public override string ToString()
        {
            StringBuilder sb = new StringBuilder();

            Queue<IState> qState = new Queue<IState>();
            List<IState> visited = new List<IState>();

            qState.Enqueue(mStart);

            while (qState.Count > 0)
            {
                IState state = qState.Dequeue();

                bool found = false;
                foreach (IState v in visited)
                {
                    if (v == state)
                    {
                        found = true;
                        break;
                    }
                }
                if (found) continue;
                else
                    visited.Add(state);

                sb.Append(state.ToString());
                sb.Append('\n');
                int i = 0;

                foreach (IArrow arrow in state)
                {
                    IState target = arrow.Target;

                    if (target != state)
                    {
                        qState.Enqueue(target);
                    }

                    sb.Append("  [");
                    sb.Append(i);
                    sb.Append("] -- ");
                    sb.Append(arrow.ToString());
                    sb.Append(string.Format(" -> State[0x{0:X8}]\n", target.Id));

                    i++;
                }
            }

            return sb.ToString();
        }

    }   /* class Machine */

}   /* namespace QSharp.String.Rex */
